T:Type, eq:EqDecider(T), as, bs:T List, x:T.
(x  list-diff(eq;as;bs))  (x  as) & (x  bs) 

latex

Definitions	x:A. B(x), P  Q, P & Q, t  T, (x  l), A, P  Q, EqDecider(T)
Lemmas	list-diff-property, deq wf